$\forall$$T$, $A$:Type, $x$:$T$, ${\it eq}$:EqDecider($T$). $A$ $\Rightarrow$ non{-}void($x$ : $A$)